package derivable;

import java.util.Collection;
import java.util.Collections;
import java.util.HashSet;
import java.util.Objects;
import java.util.Set;

/**
 * @author Henrik Wall
 * @author Rudolf Schmidt
 * @author Eugen Nemirowski
 */
public final class Disjunction implements Derivable<Disjunction>, Symbolized {
	private static final String SYMBOL = "|";
	
	private final Set<Conjunction> conjunctions;

	private Disjunction(final Set<Conjunction> conjunctions) {
		this.conjunctions = conjunctions;
	}

	/**
	 * Creates a new {@link Disjunction} of all the {@link Conjunction}s.
	 * 
	 * @param propositions to be disjunct
	 * @return a new {@link Disjunction}
	 */
	public static Disjunction create(final Collection<? extends Conjunction> conjunctions) {
		return new Disjunction(new HashSet<>(conjunctions));
	}

	/**
	 * Creates a new {@link Disjunction} of all the {@link Conjunction}s.
	 * 
	 * @param propositions to be disjunct
	 * @return a new {@link Disjunction}
	 */
	public static Disjunction create(final Conjunction... conjunctions) {
		final Set<Conjunction> cs = new HashSet<>();
		Collections.addAll(cs, conjunctions);
		return new Disjunction(cs);
	}

	/**
	 * For {@link Disjunction}s d = {c<sub>1</sub>, …, c<sub>n</sub>} and d' =
	 * {c'<sub>1</sub>, …, c'<sub>m</sub>}: derives(d, d'): <=> For all i exists
	 * one j: derives(c<sub>i</sub>, c<sub>j</sub>')
	 */
	@Override
	public boolean derives(final Disjunction o) {
		i: for (final Conjunction ci : conjunctions) {
			for (final Conjunction cj : o.conjunctions) {
				if (ci.derives(cj))
					continue i;
			}
			return false;
		}
		return true;
	}

	@Override
	public String getSymbol() {
		return SYMBOL;
	}

	@Override
	public int hashCode() {
		final int prime = 31;
		int result = 1;
		result = prime * result + Objects.hashCode(conjunctions);
		return result;
	}

	@Override
	public boolean equals(Object obj) {
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		final Disjunction other = (Disjunction) obj;
		return Objects.equals(conjunctions, other.conjunctions);
	}

	@Override
	public String toString() {
		if (conjunctions.isEmpty()) {
			return "()";
		}
		final StringBuilder sb = new StringBuilder("(");
		for (final Conjunction conjunction : conjunctions) {
			sb.append(conjunction);
			sb.append(getSymbol());
		}
		sb.setLength(sb.length() - getSymbol().length());
		return sb.append(")").toString();
	}
}